i:Id, T:Type{i}, s:T, R:(TTProp{i'}), poss:(ES{i}Prop{i'}), ev:possible-event{i:l}(poss).
poss-consistent(i;T;s;ev;R)  Prop{i'} 

latex

Definitions	Id, t  T, Type, Prop, x:AB(x), ES, x:A. B(x), PossibleEvent(poss), pe-es(e), state@i, pe-state(p), P & Q, f(a), pe-loc(p), s = t, x:AB(x), A & B, poss-consistent(i;T;s;ev;R), {T}, P  Q, SQType(T), s ~ t, Atom$n
Lemmas	Id sq, pe-loc wf, es-state wf, pe-es wf, pe-state wf, possible-event wf, event system wf, Id wf